Nuprl Lemma : better-w-m-wf
0,22
postcript
pdf
the_w
:World,
i
:Id,
t
:
. m(
i
;
t
)
MsgFrom(
i
) List
latex
Definitions
Id
,
t
T
,
,
x
:
A
.
B
(
x
)
,
w
.M
,
Msg
,
m(
i
;
t
)
,
MsgFrom(
i
)
,
World
Lemmas
world
wf
,
nat
wf
,
Id
wf
origin
the_w:World, i:Id, t:
. m(i;t) 
MsgFrom(i) List the_w:World, i:Id, t:. m(i;t) MsgFrom(i) List Tx:A. B(x)